when-after(e;info;pred?;init;Trans;val;time)
== if first(e)
== then let s = x.init(loc(e),x)+time(e) in <s, Trans(loc(e),kind(e),val(e),s)>
== else let s = when-after(pred(e);info;pred?;init;Trans;val;time).2+(time(e)) - (time(pred(e))) in
== else let s<s, Trans(loc(e),kind(e),val(e),s)>
== fi 

---

clarification:

when-after(e;info;pred?;init;Trans;val;time)
== if first(pred?;e)
== then let s = x.init(loc(info;e),x)+time(e) in <s, Trans(loc(info;e),kind(info;e),val(e),s)>
== else let s = when-after(pred(pred?;e);info;pred?;init;Trans;val;time).2
== else let s = +(time(e)) - (time(pred(pred?;e))) in <s, Trans(loc(info;e),kind(info;e),val(e),s)>
== fi 
(recursive) 

latex

Definitions	Y, if b then t else f fi , first(e), x.A(x), let x = a in b(x), s+r, t.2, r - s, pred(e), <a, b>, loc(e), kind(e), f(a)
FDL editor aliases	when-after